\begin{tabbing}
$\forall$$D$:Dsys.
\\[0ex]Feasible($D$)
\\[0ex]$\Rightarrow$ (\=$\exists$${\it sched}$:(Id$\rightarrow$($\mathbb{N}\rightarrow$(IdLnk+Id)+Unit)).\+
\\[0ex]$\forall$$i$:Id.
\\[0ex](\=$\forall$$l$:IdLnk.\+
\\[0ex]destination($l$) $=$ $i$
\\[0ex]$\Rightarrow$ M(source($l$)) sends on link $l$
\\[0ex]$\Rightarrow$ \=isl(${\it sched}$($i$))\+
\\[0ex]\& ($\forall$$t$:$\mathbb{N}$. $\exists$${\it t'}$:$\mathbb{N}$. $t$$\leq$${\it t'}$ \& isl(outl(${\it sched}$($i$))(${\it t'}$)) \& outl(outl(${\it sched}$($i$))(${\it t'}$)) $=$ $l$))
\-\-\\[0ex]\& (\=$\forall$$a$:Id.\+
\\[0ex]$a$ in dom(M($i$).pre)
\\[0ex]$\Rightarrow$ \=isl(${\it sched}$($i$))\+
\\[0ex]\& (\=$\forall$$t$:$\mathbb{N}$.\+
\\[0ex]$\exists$${\it t'}$:$\mathbb{N}$. $t$$\leq$${\it t'}$ \& $\neg_{2}$isl(outl(${\it sched}$($i$))(${\it t'}$)) \& outr(outl(${\it sched}$($i$))(${\it t'}$)) $=$ $a$)))
\-\-\-\-
\end{tabbing}